\section{Repressilator}\label{app:repressilator}

Figure \ref{fig:repress} gives the Petri net for the \andy system given in Example \ref{ex:rep}.
The Petri net representation is obtained via the Snakes library.

\begin{figure}[ht]
 \centering
 \includegraphics[width=0.9\textwidth]{repress.png}
\caption{\andy network for the Repressilator}\label{fig:repress}
\end{figure}


\section{Mobile phone battery example}\label{ex:battery}
  %
      Take the battery of a mobile phone.  We identify its
      electric capacity as an entity having a few charge levels. For the
      sake of the example, say $5$ levels from $0$ the minimal level of
      charge to $4$ meaning full charge. The evolution of the charge
      level along time is subject to the following constraints:
      \begin{enumerate}

      \item \label{it:decay} The level of mobile phone charge diminishes
            continuously, even when it is not used for making a phone
            call; it diminishes slowly when it is fully charged and
            faster when it is partly discharged;

      \item \label{it:plug} The mobile phone may be plugged to start
            charging, which takes some time to reach full charge;

      \item \label{it:call} If charged enough, the mobile phone may be
            used to make phone calls but its charge diminishes;

      \item \label{it:GPS} Similarly, GPS navigation needs more charge
            and consumes battery faster.
      \end{enumerate}
      Item~(\ref{it:decay}) corresponds to the decay process, while the
      other three items represent activity rules. Item (\ref{it:plug})
      is modeled with an auxiliary entity representing the plug (which
      may be on or off). The action of plugging the mobile phone is a
      \potential activity. If plugged the battery starts charging which
      is represented by a \obligatory activity augmenting its charge
      level. Items~(\ref{it:call}) and~(\ref{it:GPS}) are implemented
      similarly, using two more entities one for the call and the other
      for the GPS navigation.   

 \paragraph{\bf Entities.}     A mobile phone is characterized by four observables with corresponding number of levels and associated decay:
      $$ \begin{array}{rcll}
            \text{Battery}  
            & ~~B~~ 
            & \setlev_{B} = 5
            & \life_{B}(i)=2 \text{ for }  0<i \leq 3,  \quad
            \life_{B}(4)=3
            \\
            \text{Plug} 
            & P 
            & \setlev_{P} = 2 
            &  
            \\
            \text{Call} 
            & C 
            & \setlev_{C} = 2 
            &  
            \\
            \text{GPS} 
            & G 
            & \setlev_{G} = 2 \ 
            &  
      \end{array}
      $$
      %%
      where unspecified decays are all set to $\omega$.  Decay
      durations are used to model Item (\ref{it:decay}) above. Notice that in the modeling of charge $B$,
      delays are not uniform to denote different speeds in the
      consumption of the charge (\ie for the full charge level 4 decay
      takes 3 units of time while for the others it is 2).  All other
      entities have only two levels, roughly speaking
      \emph{on}/\emph{off}, encoded as 0 for \emph{off} and 1 for
      \emph{on}. The environment has no role in the evolution of the
      levels of these observables that are therefore set to unbounded
      duration $\omega$.  

\paragraph{\bf Activities.}      The constraints specified by Items (2-4) above give rise to the following sets of
      activities.

      Item (\ref{it:plug}) may be described by two \potential
      instantaneous activities, $\alpha_1$ and $\alpha_2$, which model
      plugging and unplugging respectively, and a \obligatory activity
      $\beta_1$ with duration 1 that models the charging process.
      $$
      \begin{array}{ll ll}
        \alpha_1: & \activ{(P,0)}{(P,1)}{0}{(P,+1)} 
        \qquad & \beta_1: & \activ{(P,1)}{\emptyset}{1}{(B,+1)}  \\
         \alpha_2: & \activ{(P,1)}{\emptyset}{0}{(P,-1)}   
      \end{array}
      $$

      Similarly, Item (\ref{it:call}) may be depicted by two
      \potential instantaneous activities, $\alpha_3$ and $\alpha_4$,
      modeling the start and the end of a phone call respectively, and
      a \obligatory activity $\beta_2$ with duration 3 defining the
      discharging process due to such a call.\looseness=-1
      %% 
      $$
      \begin{array}{ll ll}
            \alpha_3: & \activ{(C,0)}{(C,1)}{0}{(C,+1)} 
            \qquad & \beta_2: & \activ{(C,1)}{\emptyset}{3}{(B,-1)} \\
            \alpha_4: & \activ{(C,1)}{\emptyset}{0}{(C,-1)} 
      \end{array}
      $$

      Finally Item (\ref{it:GPS}) may again be described by two
      \potential instantaneous activities, $\alpha_5$ and $\alpha_6$,
      that model activation and deactivation of GPS navigation
      respectively, and a \obligatory activity $\beta_3$ with
      duration 3 that models the discharging process due to the GPS
      usage. Notice that in this case, even if duration is the same,
      the battery is consumed faster than a simple phone call
      (indicated by $(B, -2)$ instead of $(B, -1)$).
      $$
      \begin{array}{ll ll}
            \alpha_5: & \activ{(G,0)}{(G,1)}{0}{(G,+1)}
            \qquad &  \beta_3: & \activ{(G,1)}{\emptyset}{3}{(B,-2)} \\
            \alpha_6: & \activ{(G,1)}{\emptyset}{0}{(G,-1)} 
      \end{array}
      $$
      \paragraph{\bf Initial state and execution
      scenario.}
			
We illustrate the functioning of an \andy network on the
following scenario starting from the initial levels: 
$(B, 4)$, $(P, 0)$, $(C, 0)$, $(G,0)$, see Figure~\ref{fig:diagram}:



\begin{figure}[t]
\centering
\begin{tikzpicture}[>=latex',xscale=.8, yscale=.5]

\draw[draw=none,fill=blue!10] (-1,1) rectangle (11,2) ; 
\draw[draw=none,fill=blue!10] (-1,3) rectangle (11,4) ; 
\draw[draw=none,fill=blue!10] (-1,5) rectangle (11,6) ; 
\draw[draw=none,fill=blue!10] (-1,7) rectangle (11,8) ; 
\draw[draw=none,fill=blue!10] (-1,9) rectangle (11,10) ; 

\node at (-1,1) (p0) {};
\node[left] at (p0.west) {$0$};
\node at (-1,2) (p1) {};
\node[left] at (p1.west) {$1$};
\node at (-1,3) (c0) {};
\node[left] at (c0.west) {$0$};
\node at (-1,4) (c1) {};
\node[left] at (c1.west) {$1$};
\node at (-1,5) (g0) {};
\node[left] at (g0.west) {$0$};
\node at (-1,6) (g1) {};
\node[left] at (g1.west) {$1$};
\node at (-1,7) (b0) {};
\node[left] at (b0.west) {$0$};
\node at (-1,8) (b1) {};
\node[left] at (b1.west) {$1$};
\node at (-1,9) (b2) {};
\node[left] at (b2.west) {$2$};
\node at (-1,10) (b3) {};
\node[left] at (b3.west) {$3$};

\node[label=left:{$B=\left[ \phantom{\begin{array}{l} a\\ a\\ a\\ a \end{array}} \right.$}] at (-1,8.5) (b) {};
\node[label=left:{$G=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,5.5) (g) {};
\node[label=left:{$C=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,3.5) (c) {};
\node[label=left:{$P=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,1.5) (p) {};

%\draw[->] (p0) -- (p1) ;
%\draw[->] (c0) -- (c1) ;
%\draw[->] (g0) -- (g1) ;
%\draw[->] (b0) -- (b3) ;

%points horizontaux
\node at (-2,0) (t0) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:0] at (0,0) (t1) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:1] at (2,0) (t2) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:2] at (4,0) (t3) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:3] at (6,0) (t4) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:4] at (8,0) (t5) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:5] at (10,0) (t6) {};
\node[label=below:$time$] at (11,0) (t7) {};

% points verticaux
\node[rectangle,draw,fill=blue,scale=.3] at (-1,1) (k1) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,2) (k2) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,3) (k3) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,4) (k4) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,5) (k5) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,6) (k6) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,7) (k7) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,8) (k8) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,9) (k9) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,10) (k10) {};

\draw[->] (t0) -- (t7) ; %axe du temps
\draw[->] (-1,0) -- (-1,11.5) ; %axe vertical

\path[draw,thick] (0,1) --(6,1) --node[midway,above,sloped]{$\alpha_1$} (6,2) -- (9,2) ;
\node[right] at (9,2) {$\cdots$};
\path[draw,thick] (0,3)  --node[midway,above,sloped]{$\alpha_3$} (0,4) -- (9,4) ;
\node[right] at (9,4) {$\cdots$};
\path[draw,thick] (0,5) --node[midway,above, sloped]{$\alpha_5$}  (0,6) -- (9,6) ;
\node[right] at (9,6) {$\cdots$};
\path[draw,thick] (0,10) -- (6,10) -- (6,7) -- (8,7) -- (8,9) -- (9,9) ;
\node[right] at (9,9) {$\cdots$};
\node[above] at (6,10) {$\beta_2,\beta_3,decay$};
\node[above] at (8,9) {$\beta_1$};

\end{tikzpicture}
\caption{Entities levels evolving with time corresponding to the given scenario.}
\label{fig:diagram}
\end{figure}

      \begin{enumerate}

      \item Activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)

      \item Start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)

      \item Three time units pass by -- no decay or \obligatory activities are involved

      \item One time unit passes by -- battery decays and enabled \obligatory
            activities\\
            %
            $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}$ and
            $\beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$
            %
            are performed

      \item Plug the phone ($\alpha_1: \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)

      \item One time unit passes by -- no decay but enabled
        \obligatory activity
        $\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed 
      \end{enumerate}
      


\paragraph{\bf  Execution scenario.}
We illustrate the evolution of tuples of counters $\birth{}$ starting from 
the initial state, we have the following sequence of markings:
$$
\begin{array}{ccccc}
 & p_B &p_P&p_C&p_G\\
\mathit{init} & \quad \tuple{4, 0, [0,0,0,0,0]} \quad 
 & \quad \tuple{0, 0, [0,0]} \quad 
 &\quad  \tuple{0, 0, [0,0]}\quad 
 &\quad  \tuple{0, 0, [0,0]}\quad \\
%we activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)
1 & \quad \tuple{4, 0, [0,0,0,0,0]}\quad
 &\quad \tuple{0, 0, [0,0]}\quad
&\quad \tuple{0, 0, [0,0]}\quad
 &\quad \tuple{1, 0, [0,0]}\quad \\
%start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)
2 & \quad \tuple{4, 0, [0,0,0,0,0]} \quad
& \quad \tuple{0, 0, [0,0]} \quad
 &\quad \tuple{1, 0, [0,0]}\quad
 &\quad \tuple{1, 0, [0,0]}\quad \\
%3 time units pass by (no decay or obligatory activity involved)
3 & \quad
 \tuple{4, 3, [3,3,3,3,3]} \quad
& \quad \tuple{0, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]}\quad \\
% 1 time unit pass by, battery decays, and enabled obligatory activities\\ $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}, \beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$ are performed
4 & \quad
 \tuple{0, 0, [0,0,0,0,0]} \quad
& \quad \tuple{0, 0, [3,3]}\quad
& \quad \tuple{1, 0, [3,3]}\quad
& \quad \tuple{1, 3, [3,3]}\quad \\
%we plug the phone ($\alpha_1:  \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)
5 & \quad
 \tuple{0, 0, [0,0,0,0,0]} \quad
& \quad \tuple{1, 0, [3,0]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]} \quad \\
% 1 time unit passes by with no decays and enabled obligatory activity\\
%\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed
6 & \quad
 \tuple{1, 0, [1,0,1,1,1]} \quad
 &\quad \tuple{1, 0, [3,1]} \quad
 &\quad \tuple{1, 0, [3,3]} \quad
 &\quad \tuple{1, 0, [3,3]} 
\end{array}
$$

Figure \ref{fig:snakesbattery} shows the SNAKES Petri net rendering of the mobile phone example.

\begin{figure}[t]


{\centering
\scalebox{0.33}{
\begin{tikzpicture}[>=latex',line join=bevel,scale=0.7]
%%
\definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_13) at (1218.6bp,361bp) [draw,fill=fillcolor,rectangle] {tr1};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_14) at (1206.6bp,151bp) [draw,fill=fillcolor,rectangle] {tr0};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_18) at (943.65bp,571bp) [draw,fill=fillcolor,rectangle] {tc: True};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_19) at (714.65bp,361bp) [draw,fill=fillcolor,rectangle] {tr4};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_9) at (1393.6bp,676bp) [draw,fill=fillcolor,ellipse] {ptr0: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_8) at (331.65bp,466bp) [draw,fill=fillcolor,ellipse] {ptr3: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_7) at (520.65bp,46bp) [draw,fill=fillcolor,ellipse] {ptr2: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_6) at (851.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob2: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_5) at (1006.6bp,466bp) [draw,fill=fillcolor,ellipse] {ptr4: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_4) at (103.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob0: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_3) at (219.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob1: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_2) at (699.65bp,256bp) [draw,fill=fillcolor,ellipse] {G: \{(0, 0, (0, 0))\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_1) at (663.65bp,466bp) [draw,fill=fillcolor,ellipse] {B: \{(4, 0, (0, 0, 0, 0, 0))\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_0) at (183.65bp,256bp) [draw,fill=fillcolor,ellipse] {C: \{(0, 0, (0, 0))\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_17) at (745.65bp,151bp) [draw,fill=fillcolor,rectangle] {tr5};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_11) at (887.65bp,46bp) [draw,fill=fillcolor,ellipse] {ptr5: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_16) at (282.65bp,151bp) [draw,fill=fillcolor,rectangle] {tr2};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_10) at (1226.6bp,466bp) [draw,fill=fillcolor,ellipse] {ptr1: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_15) at (209.65bp,361bp) [draw,fill=fillcolor,rectangle] {tr3};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_12) at (1158.6bp,256bp) [draw,fill=fillcolor,ellipse] {P: \{(0, 0, (0, 0))\}};
  \draw [->,solid] (node_4) ..controls (53.011bp,500.46bp) and (38.13bp,517.88bp)  .. (51.647bp,532bp) .. controls (81.223bp,562.9bp) and (723bp,569.51bp)  .. (node_18);
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (75.647bp,523bp) node { $wob_0$};
  \draw [->,solid] (node_18) ..controls (1038.5bp,561.15bp) and (1159.3bp,546.66bp)  .. (1171.6bp,532bp) .. controls (1176.8bp,525.88bp) and (1175.9bp,520.78bp)  .. (1171.6bp,514bp) .. controls (1161.9bp,498.5bp) and (1148.7bp,507.72bp)  .. (1134.6bp,496bp) .. controls (1109.3bp,474.81bp) and (1118.7bp,453.59bp)  .. (1090.6bp,436bp) .. controls (1053.5bp,412.68bp) and (1021.7bp,451.71bp)  .. (993.65bp,418bp) .. controls (993.65bp,418bp) and (993.65bp,340bp)  .. (993.65bp,340bp) .. controls (970.26bp,310.93bp) and (935.71bp,350.52bp)  .. (911.65bp,322bp) .. controls (897.88bp,305.68bp) and (905.03bp,151.22bp)  .. (902.65bp,130bp) .. controls (901bp,115.31bp) and (898.36bp,99.311bp)  .. (node_11);
  \draw (969.65bp,313bp) node { min(D,wtr5+1)};
  \draw [->,solid] (node_5) ..controls (964.3bp,442.46bp) and (955.34bp,438.64bp)  .. (946.65bp,436bp) .. controls (885.78bp,417.51bp) and (864.51bp,439.53bp)  .. (804.65bp,418bp) .. controls (785.12bp,410.97bp) and (765.42bp,399.16bp)  .. (node_19);
  \draw (815.65bp,409bp) node { w};
  \draw [->,solid] (node_9) ..controls (1265.4bp,646.08bp) and (1074.2bp,601.47bp)  .. (node_18);
  \draw (1204.1bp,619bp) node { wtr0};
  \draw [->,solid] (node_19) ..controls (733.51bp,329.2bp) and (737.44bp,315.93bp)  .. (733.65bp,304bp) .. controls (732.5bp,300.38bp) and (730.96bp,296.8bp)  .. (node_2);
  \draw (798.15bp,313bp) node { ($l_G$,$u_G$,$\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (976.99bp,539.38bp) and (983.9bp,526.2bp)  .. (977.65bp,514bp) .. controls (971.41bp,501.81bp) and (961.45bp,506.49bp)  .. (952.65bp,496bp) .. controls (933.6bp,473.32bp) and (948.29bp,452.43bp)  .. (923.65bp,436bp) .. controls (893.74bp,416.06bp) and (636.01bp,424.46bp)  .. (600.65bp,418bp) .. controls (574.51bp,413.22bp) and (569.43bp,406.41bp)  .. (543.65bp,400bp) .. controls (522.16bp,394.66bp) and (459.82bp,399.01bp)  .. (445.65bp,382bp) .. controls (433.7bp,367.66bp) and (433.43bp,354.12bp)  .. (445.65bp,340bp) .. controls (482.09bp,297.89bp) and (519.87bp,346.96bp)  .. (569.65bp,322bp) .. controls (579.76bp,316.93bp) and (578.28bp,310.34bp)  .. (587.65bp,304bp) .. controls (600.65bp,295.2bp) and (615.53bp,287.46bp)  .. (node_2);
  \draw (663.15bp,409bp) node { ($l_G$,$u_G$,$\lambda_G$)};
  \draw [->,solid] (node_10) ..controls (1302.9bp,485.07bp) and (1346.3bp,499.1bp)  .. (1356.6bp,514bp) .. controls (1361.2bp,520.56bp) and (1362bp,526.08bp)  .. (1356.6bp,532bp) .. controls (1332.2bp,558.88bp) and (1089.5bp,567.62bp)  .. (node_18);
  \draw (1382.1bp,523bp) node { wtr1};
  \draw [->,solid] (node_8) ..controls (299.73bp,426.93bp) and (285.77bp,411.83bp)  .. (271.65bp,400bp) .. controls (266.54bp,395.72bp) and (260.92bp,391.56bp)  .. (node_15);
  \draw (300.65bp,409bp) node { w};
  \draw [->,solid] (node_18) ..controls (820.19bp,564.49bp) and (585.46bp,550.33bp)  .. (555.65bp,532bp) .. controls (502.72bp,499.46bp) and (554.78bp,442.7bp)  .. (509.65bp,400bp) .. controls (477.16bp,369.26bp) and (445.07bp,410.55bp)  .. (410.65bp,382bp) .. controls (382.83bp,358.93bp) and (372.19bp,336.67bp)  .. (387.65bp,304bp) .. controls (427.23bp,220.36bp) and (509.06bp,255.64bp)  .. (548.65bp,172bp) .. controls (562.05bp,143.68bp) and (552.46bp,108.7bp)  .. (node_7);
  \draw (445.65bp,313bp) node { min(D,wtr2+1)};
  \draw [->,solid] (node_14) ..controls (1381.8bp,177.1bp) and (1399.4bp,183.04bp)  .. (1408.6bp,190bp) .. controls (1435.1bp,209.78bp) and (1442.6bp,223bp)  .. (1442.6bp,256bp) .. controls (1442.6bp,571bp) and (1442.6bp,571bp)  .. (1442.6bp,571bp) .. controls (1442.6bp,597.2bp) and (1438.7bp,604.26bp)  .. (1427.6bp,628bp) .. controls (1425.6bp,632.45bp) and (1423.1bp,636.92bp)  .. (node_9);
  \draw (1452.1bp,409bp) node { 0};
  \draw [->,solid] (node_17) ..controls (795.99bp,113.78bp) and (825.8bp,91.734bp)  .. (node_11);
  \draw (831.15bp,103bp) node { 0};
  \draw [->,solid] (node_12) ..controls (1226bp,284.82bp) and (1235.5bp,293.33bp)  .. (1241.6bp,304bp) .. controls (1246.5bp,312.37bp) and (1245bp,321.95bp)  .. (node_13);
  \draw (1309.1bp,313bp) node { ($l_P$, $u_P$, $\lambda_P$)};
  \draw [->,solid] (node_17) ..controls (743.02bp,183.28bp) and (740.52bp,196.75bp)  .. (735.65bp,208bp) .. controls (733.99bp,211.82bp) and (731.98bp,215.61bp)  .. (node_2);
  \draw (804.15bp,199bp) node { ($l_G$,$u_G$,$\lambda_G$)};
  \draw [->,solid] (node_13) ..controls (1135.3bp,334.36bp) and (1123.9bp,328.18bp)  .. (1119.6bp,322bp) .. controls (1113.1bp,312.37bp) and (1115.6bp,301.62bp)  .. (node_12);
  \draw (1178.6bp,313bp) node { ($l_P$,$u_P$,$\lambda_P$)};
  \draw [->,solid] (node_16) ..controls (405.16bp,125.01bp) and (421.12bp,119.11bp)  .. (435.65bp,112bp) .. controls (454.06bp,103bp) and (472.29bp,89.591bp)  .. (node_7);
  \draw (473.15bp,103bp) node { 0};
  \draw [->,solid] (node_18) ..controls (1080.2bp,569.57bp) and (1378.7bp,563.5bp)  .. (1407.6bp,532bp) .. controls (1413.1bp,526.11bp) and (1411.5bp,521.02bp)  .. (1407.6bp,514bp) .. controls (1398.1bp,496.64bp) and (1267.1bp,435.36bp)  .. (1257.6bp,418bp) .. controls (1253.8bp,410.98bp) and (1252.4bp,406.08bp)  .. (1257.6bp,400bp) .. controls (1291.6bp,360.38bp) and (1338.7bp,420.76bp)  .. (1373.6bp,382bp) .. controls (1396.9bp,356.23bp) and (1398.4bp,331.04bp)  .. (1376.6bp,304bp) .. controls (1360.5bp,283.92bp) and (1302.4bp,271.75bp)  .. (node_12);
  \draw (1316.6bp,409bp) node { ($l_P$,$u_P$,$\lambda_P$)};
  \draw [->,solid] (node_11) ..controls (908.91bp,100.58bp) and (925.29bp,139.6bp)  .. (942.65bp,172bp) .. controls (975.6bp,233.51bp) and (1006.8bp,237.41bp)  .. (1027.6bp,304bp) .. controls (1042.8bp,352.38bp) and (999bp,379.22bp)  .. (1031.6bp,418bp) .. controls (1056.8bp,447.87bp) and (1087.2bp,411.53bp)  .. (1117.6bp,436bp) .. controls (1140.4bp,454.32bp) and (1124.6bp,474.67bp)  .. (1144.6bp,496bp) .. controls (1156.3bp,508.47bp) and (1169.8bp,499.35bp)  .. (1178.6bp,514bp) .. controls (1182.8bp,520.85bp) and (1183.8bp,525.9bp)  .. (1178.6bp,532bp) .. controls (1166.5bp,546.34bp) and (1053bp,559.99bp)  .. (node_18);
  \draw (1053.1bp,313bp) node { wtr5};
  \draw [->,solid] (node_18) ..controls (784.54bp,566.41bp) and (356.04bp,552.46bp)  .. (335.65bp,532bp) .. controls (328.73bp,525.06bp) and (325.98bp,515.41bp)  .. (node_8);
  \draw (393.65bp,523bp) node { min(D,wtr3+1)};
  \draw [->,solid] (node_0) ..controls (85.22bp,284.04bp) and (60.359bp,300.25bp)  .. (76.647bp,322bp) .. controls (80.619bp,327.3bp) and (89.039bp,332.13bp)  .. (node_15);
  \draw (141.65bp,313bp) node { ($l_C$, $u_C$, $\lambda_C$)};
  \draw [->,solid] (node_15) ..controls (210.44bp,328.99bp) and (209.61bp,315.62bp)  .. (206.65bp,304bp) .. controls (205.84bp,300.82bp) and (204.81bp,297.6bp)  .. (node_0);
  \draw (270.15bp,313bp) node { ($l_C$,$u_C$,$\lambda_C$)};
  \draw [->,solid] (node_7) ..controls (444.49bp,79.598bp) and (384.15bp,106.22bp)  .. (node_16);
  \draw (420.65bp,103bp) node { w};
  \draw [->,solid] (node_15) ..controls (227.95bp,393.76bp) and (237.57bp,407.73bp)  .. (248.65bp,418bp) .. controls (252.21bp,421.31bp) and (269.82bp,431.6bp)  .. (node_8);
  \draw (258.15bp,409bp) node { 0};
  \draw [->,solid] (node_12) ..controls (1115.8bp,300.47bp) and (1097.9bp,318.64bp)  .. (1093.6bp,322bp) .. controls (1081.4bp,331.62bp) and (1073.9bp,328.31bp)  .. (1063.6bp,340bp) .. controls (1050.6bp,354.9bp) and (1028.8bp,407.59bp)  .. (1037.6bp,418bp) .. controls (1068.8bp,454.82bp) and (1106.3bp,406.8bp)  .. (1144.6bp,436bp) .. controls (1168.1bp,453.82bp) and (1151.9bp,475.13bp)  .. (1172.6bp,496bp) .. controls (1175.1bp,498.48bp) and (1236.5bp,502.11bp)  .. (1210.6bp,532bp) .. controls (1196.3bp,548.59bp) and (1060bp,561.78bp)  .. (node_18);
  \draw (1101.1bp,409bp) node { ($l_P$, $u_P$, $\lambda_P$)};
  \draw [->,solid] (node_0) ..controls (282.79bp,277.88bp) and (311.35bp,288.61bp)  .. (334.65bp,304bp) .. controls (352.26bp,315.64bp) and (356.57bp,320.93bp)  .. (365.65bp,340bp) .. controls (380.78bp,371.8bp) and (360.63bp,388.35bp)  .. (379.65bp,418bp) .. controls (419.98bp,480.89bp) and (467.54bp,458.58bp)  .. (517.65bp,514bp) .. controls (523.78bp,520.79bp) and (519.98bp,527bp)  .. (527.65bp,532bp) .. controls (558.26bp,551.99bp) and (798.68bp,564.68bp)  .. (node_18);
  \draw (444.65bp,409bp) node { ($l_C$, $u_C$, $\lambda_C$)};
  \draw [->,solid] (node_2) ..controls (604.93bp,226.72bp) and (581.75bp,210.63bp)  .. (597.65bp,190bp) .. controls (601.83bp,184.57bp) and (610.33bp,179.75bp)  .. (node_17);
  \draw (664.65bp,199bp) node { ($l_G$, $u_G$, $\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (760.09bp,567.16bp) and (169.47bp,553.4bp)  .. (136.65bp,532bp) .. controls (126.77bp,525.56bp) and (119.73bp,515.22bp)  .. (node_4);
  \draw (160.65bp,523bp) node { $wob_0$};
  \draw [->,solid] (node_11) ..controls (822.18bp,63.667bp) and (794.36bp,75.603bp)  .. (774.65bp,94bp) .. controls (766.85bp,101.27bp) and (760.83bp,111.11bp)  .. (node_17);
  \draw (785.65bp,103bp) node { w};
  \draw [->,solid] (node_14) ..controls (1223.1bp,183.15bp) and (1226.2bp,196.75bp)  .. (1220.6bp,208bp) .. controls (1217.9bp,213.69bp) and (1214bp,218.91bp)  .. (node_12);
  \draw (1282.6bp,199bp) node { ($l_P$,$u_P$,$\lambda_P$)};
  \draw [->,solid] (node_18) ..controls (749.02bp,569.86bp) and (73.172bp,563.87bp)  .. (42.647bp,532bp) .. controls (-27.86bp,458.37bp) and (-3.6588bp,376.85bp)  .. (67.647bp,304bp) .. controls (78.465bp,292.95bp) and (92.197bp,284.33bp)  .. (node_0);
  \draw (66.147bp,409bp) node { ($l_C$,$u_C$,$\lambda_C$)};
  \draw [->,solid] (node_16) ..controls (178.59bp,177.36bp) and (166.45bp,183.4bp)  .. (161.65bp,190bp) .. controls (155.67bp,198.2bp) and (155.99bp,208.13bp)  .. (node_0);
  \draw (222.15bp,199bp) node { ($l_C$,$u_C$,$\lambda_C$)};
  \draw [->,solid] (node_5) ..controls (996.74bp,507.27bp) and (991.71bp,520.89bp)  .. (984.65bp,532bp) .. controls (982.39bp,535.54bp) and (979.75bp,538.99bp)  .. (node_18);
  \draw (1015.1bp,523bp) node { wtr4};
  \draw [->,solid] (node_18) ..controls (966.39bp,604.78bp) and (979.81bp,619.84bp)  .. (995.65bp,628bp) .. controls (1054.2bp,658.14bp) and (1243.5bp,669.95bp)  .. (node_9);
  \draw (1053.6bp,619bp) node { min(D,wtr0+1)};
  \draw [->,solid] (node_19) ..controls (725.25bp,394.71bp) and (733.12bp,409.78bp)  .. (745.65bp,418bp) .. controls (783.13bp,442.61bp) and (903.5bp,423.76bp)  .. (946.65bp,436bp) .. controls (952.32bp,437.61bp) and (958.09bp,439.75bp)  .. (node_5);
  \draw (755.15bp,409bp) node { 0};
  \draw [->,solid] (node_1) ..controls (683.76bp,508.72bp) and (694.11bp,523.26bp)  .. (707.65bp,532bp) .. controls (738.58bp,551.97bp) and (839.92bp,562.99bp)  .. (node_18);
  \draw (772.65bp,523bp) node { ($l_B$, $u_B$, $\lambda_B$)};
  \draw [->,solid] (node_13) ..controls (1216.3bp,387.85bp) and (1215.9bp,394.16bp)  .. (1215.6bp,400bp) .. controls (1215.3bp,407.99bp) and (1214.7bp,410.05bp)  .. (1215.6bp,418bp) .. controls (1216bp,420.87bp) and (1216.4bp,423.81bp)  .. (node_10);
  \draw (1225.1bp,409bp) node { 0};
  \draw [->,solid] (node_2) ..controls (800.88bp,279.54bp) and (835.16bp,290.28bp)  .. (864.65bp,304bp) .. controls (877.72bp,310.08bp) and (878.31bp,316.51bp)  .. (891.65bp,322bp) .. controls (930.17bp,337.86bp) and (957.17bp,307.83bp)  .. (983.65bp,340bp) .. controls (995.51bp,354.41bp) and (995.94bp,367.95bp)  .. (983.65bp,382bp) .. controls (944.09bp,427.23bp) and (889.21bp,354.77bp)  .. (849.65bp,400bp) .. controls (844.38bp,406.02bp) and (844.24bp,412.11bp)  .. (849.65bp,418bp) .. controls (881.48bp,452.66bp) and (1019bp,414.04bp)  .. (1060.6bp,436bp) .. controls (1091.1bp,452.07bp) and (1081.3bp,476.53bp)  .. (1109.6bp,496bp) .. controls (1130.9bp,510.55bp) and (1149.6bp,493.18bp)  .. (1164.6bp,514bp) .. controls (1169.3bp,520.48bp) and (1169.8bp,525.87bp)  .. (1164.6bp,532bp) .. controls (1142.6bp,558.33bp) and (1046bp,566.89bp)  .. (node_18);
  \draw (916.65bp,409bp) node { ($l_G$, $u_G$, $\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (999.92bp,562.32bp) and (1026.7bp,552.6bp)  .. (1040.6bp,532bp) .. controls (1047.6bp,521.72bp) and (1044.5bp,509.84bp)  .. (node_5);
  \draw (1102.6bp,523bp) node { min(D,wtr4+1)};
  \draw [->,solid] (node_0) ..controls (262.14bp,230.25bp) and (274.64bp,220.79bp)  .. (282.65bp,208bp) .. controls (287.37bp,200.47bp) and (288.77bp,191.2bp)  .. (node_16);
  \draw (353.65bp,199bp) node { ($l_C$, $u_C$, $\lambda_C$)};
  \draw [->,solid] (node_6) ..controls (884.99bp,498.11bp) and (892.8bp,506.21bp)  .. (899.65bp,514bp) .. controls (907.36bp,522.77bp) and (915.3bp,532.73bp)  .. (node_18);
  \draw (937.65bp,523bp) node { $wob_2$};
  \draw [->,solid] (node_10) ..controls (1184.6bp,438.31bp) and (1175.7bp,428.94bp)  .. (1170.6bp,418bp) .. controls (1165.9bp,407.73bp) and (1170bp,397.83bp)  .. (node_13);
  \draw (1181.6bp,409bp) node { w};
  \draw [->,solid] (node_18) ..controls (820.66bp,567.2bp) and (587.55bp,557.38bp)  .. (564.65bp,532bp) .. controls (551.56bp,517.5bp) and (561.64bp,504.71bp)  .. (node_1);
  \draw (625.15bp,523bp) node { ($l_B$,$u_B$,$\lambda_B$)};
  \draw [->,solid] (node_18) ..controls (1047.3bp,562.87bp) and (1200.9bp,548.8bp)  .. (1217.6bp,532bp) .. controls (1224.6bp,525bp) and (1227.9bp,515.33bp)  .. (node_10);
  \draw (1285.6bp,523bp) node { min(D,wtr1+1)};
  \draw [->,solid] (node_3) ..controls (188.81bp,505.35bp) and (183.22bp,521.01bp)  .. (193.65bp,532bp) .. controls (218.03bp,557.68bp) and (741.2bp,567.86bp)  .. (node_18);
  \draw (217.65bp,523bp) node { $wob_1$};
  \draw [->,solid] (node_8) ..controls (396.05bp,487.39bp) and (426.46bp,499.5bp)  .. (451.65bp,514bp) .. controls (462.9bp,520.48bp) and (462.56bp,527.26bp)  .. (474.65bp,532bp) .. controls (551.24bp,562.02bp) and (797.54bp,568.94bp)  .. (node_18);
  \draw (496.15bp,523bp) node { wtr3};
  \draw [->,solid] (node_2) ..controls (603.62bp,284.63bp) and (580.21bp,300.7bp)  .. (595.65bp,322bp) .. controls (599.35bp,327.11bp) and (607.48bp,331.9bp)  .. (node_19);
  \draw (662.65bp,313bp) node { ($l_G$, $u_G$, $\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (780.96bp,568.75bp) and (332.56bp,560.39bp)  .. (275.65bp,532bp) .. controls (262.23bp,525.31bp) and (250.76bp,513.8bp)  .. (node_3);
  \draw (299.65bp,523bp) node { $wob_1$};
  \draw [->,solid] (node_7) ..controls (546.54bp,78.888bp) and (550.82bp,86.418bp)  .. (553.65bp,94bp) .. controls (565.76bp,126.53bp) and (563.61bp,137.8bp)  .. (557.65bp,172bp) .. controls (545.47bp,241.8bp) and (556.13bp,274.39bp)  .. (503.65bp,322bp) .. controls (479.54bp,343.87bp) and (452.64bp,314.31bp)  .. (432.65bp,340bp) .. controls (421.18bp,354.73bp) and (420.83bp,367.55bp)  .. (432.65bp,382bp) .. controls (458.2bp,413.24bp) and (485.18bp,382.71bp)  .. (521.65bp,400bp) .. controls (533.06bp,405.41bp) and (531.86bp,413.46bp)  .. (543.65bp,418bp) .. controls (581.44bp,432.55bp) and (876.16bp,410.54bp)  .. (907.65bp,436bp) .. controls (929.11bp,453.35bp) and (905.59bp,475.13bp)  .. (923.65bp,496bp) .. controls (936.93bp,511.36bp) and (954.47bp,497.05bp)  .. (965.65bp,514bp) .. controls (971.02bp,522.15bp) and (969.69bp,531.81bp)  .. (node_18);
  \draw (543.15bp,313bp) node { wtr2};
  \draw [->,solid] (node_9) ..controls (1403.9bp,617.6bp) and (1410.9bp,571.91bp)  .. (1413.6bp,532bp) .. controls (1414.2bp,524.02bp) and (1414.3bp,521.98bp)  .. (1413.6bp,514bp) .. controls (1410.3bp,470.95bp) and (1404.2bp,460.82bp)  .. (1398.6bp,418bp) .. controls (1392bp,367.48bp) and (1398bp,353.66bp)  .. (1386.6bp,304bp) .. controls (1374.6bp,251.51bp) and (1385.1bp,226.68bp)  .. (1345.6bp,190bp) .. controls (1340bp,184.73bp) and (1329bp,179.73bp)  .. (node_14);
  \draw (1409.6bp,409bp) node { w};
  \draw [->,solid] (node_12) ..controls (1091.3bp,220.35bp) and (1078.5bp,205.47bp)  .. (1089.6bp,190bp) .. controls (1093.3bp,184.93bp) and (1101.4bp,180.14bp)  .. (node_14);
  \draw (1153.1bp,199bp) node { ($l_P$, $u_P$, $\lambda_P$)};
  \draw [->,solid] (node_18) ..controls (887.94bp,562.18bp) and (861.41bp,552.45bp)  .. (847.65bp,532bp) .. controls (842.37bp,524.17bp) and (840.9bp,514.55bp)  .. (node_6);
  \draw (871.65bp,523bp) node { $wob_2$};
%
\end{tikzpicture}
% End of code
}}
 \caption{SNAKES Petri net rendering of the mobile phone example.
}\label{fig:snakesbattery}  
\end{figure}


\section{Example of a High-level Petri Net}\label{app:exfiring}

Here we detail a simple example of firing. Let this be the state of the Petri net before the transition:
\begin{center}
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

  \node [place, label = left: $p_1$] at (-1.5,0) (Q1){$7$};
  \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){$5$};
  \node [place, label = right: $p_3$] at (1.5,0) (Q3){};
  
  \node [transition] (t) [  label=above : {$\begin{array}{c}
                                                x>y ~\wedge \\ x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[below] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[below]{$x'$}    (Q3);
\end{tikzpicture}
\end{center}
then by letting $\sigma = \{ x= 7, y=5, x'=12\}$,  after the firing we obtain 
\begin{center}
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

  \node [place, label = left: $p_1$] at (-1.5,0) (Q1){};
  \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){};
  \node [place, label = right: $p_3$] at (1.5,0) (Q3){12};
  
  \node [transition] (t) [  label=above:{ $\begin{array}{c}
                                                x>y~\wedge \\ x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[below] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[below]{$x'$}    (Q3);
\end{tikzpicture}
\end{center}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Encoding into Timed Automata} \label{sec:timedauto}


In this section we encode the semantics of \andy networks in terms of timed
automata. The encoding is not straightforward because of the management
of \obligatory rules. We
will show that it can be achieved at the price of an exponential translation
 in the number of activities. 

Despite this difficulty, providing a semantics in terms of timed
automata \cite{DBLP:journals/tcs/AlurD94} is appealing: since their introduction 
 they have been widely used to
model complex real time systems and to check their temporal
properties. Since then many variants have been considered depending of
synchronization policies (synchronous, urgent, broadcast \cite{uppaal}).


The main result of this section is that the semantics in term of timed
automata is equivalent to the semantics in terms of high-level Petri
net.



\paragraph{\bf Timed automata.}

A timed automaton is an annotated directed (and connected) graph, 
with an initial node and provided with a finite set of non-negative real 
variables called \emph{clocks}. 
Nodes (called \emph{locations}) are annotated with \emph{invariants} 
(predicates allowing to enter or stay in a location).
Arcs are annotated with \emph{guards}, 
\emph{communication labels}, and possibly with some clock \emph{resets}. 
Guards are conjunctions of elementary predicates of the form  
$x~\op~c$, where $\op\in\{>,\geq,=,>,\leq\}$ where $x$ is a clock and 
$c$ a (possibly parameterized) positive integer constant.
As usual, the empty conjunction is interpreted as true. 
The set of all guards and invariant predicates will be denoted by $G$. 

%In figures, locations will be represented by round nodes, the initial one having a double boundary. 

\begin{definition}\label{def:ta} A \emph{timed automaton} $\TA$
is a tuple $(L,l^0,X,\Sigma,\arcs,\inv)$, where 
\begin{itemize}
	\item $L$  is a set of locations with $l^0\in L$ the initial one, $X$ is the set of clocks, 
	\item $\Sigma=\Sigma^s\cup\Sigma^u\cup\Sigma^b$ is a set of communication labels, 
	where $\Sigma^s$ are synchronous, $\Sigma^u$ are synchronous and urgent, 
	and $\Sigma^b$ are broadcast ones,
	\item $\arcs \subseteq L \times (G \cup \Sigma \cup R) \times L$ 
is a set of arcs between locations with a guard in $G$, 
a communication label in $\Sigma\cup\{\epsilon\}$, and a set of clock resets in $R=2^X$;
for all $a\in\Sigma^u$, we require the guard to be $\true$; 
  \item $\inv: L \rightarrow G$ assigns invariants to locations. 
\end{itemize}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

It is possible to define a synchronized product of a set of timed automata 
that work and synchronize in parallel. 
The automata are required to have disjoint sets of locations, but
may share clocks and communication labels which are used for synchronization. 
We define three communication policies: 
\begin{itemize}
	\item \emph{synchronous} communications through
		labels $a\in\Sigma^s$ that require all the automata having label $a$  
		to synchronize on $a$; 
	\item \emph{synchronous urgent} communications through 
		labels $u\in\Sigma^u$ that are synchronous as above but \emph{urgent} meaning that
		there will be no delay if transition with label $u$ can be taken;
  \item \emph{broadcast} communications through labels $b!,b?\in\Sigma^b$ meaning that
	a set of automata can synchronize if one is emitting;
	notice that, a process can always emit (\eg $b!$) 
	and the receivers ($b?$) must synchronize if they can.
\end{itemize}

The synchronous product $\TA_1\parallel \ldots \parallel \TA_n$ 
of timed automata, where for each $j\in[1,\ldots,n]$, 
$\TA_j = (L_j, l^0_j,X_j,\Sigma_j,\arcs_j,\inv_j)$ and all $L_j$ are 
pairwise disjoint sets of locations is
the timed automaton $\TA=(L, l^0,X,\Sigma,\arcs,\inv)$ such that:
\begin{itemize}
\item $L=L_1\times\ldots\times L_n$ and $l^0=(l^0_1,\ldots,l^0_n)$, 
$X=\bigcup_{j=1}^n X_j$, $\Sigma=\bigcup_{j=1}^n \Sigma_j$,
\item $\forall l=(l_1, \ldots, l_n)\in L\colon \inv(l) = \bigwedge_j \inv_j(l_j)$,
\item $\arcs$ is the set of arcs 
$(l_1, \ldots, l_n) \stackrel{g,a,r}{\longrightarrow} (l'_1, \ldots, l'_n)$
such that (where for each $a\in\Sigma^s\cup\Sigma^u, 
S_a=\{j\mid 1\leq j \leq n, a\in \Sigma^s_j\cup\Sigma^u_j\}$):
	for all $1\leq j \leq n$, if $j\not\in S_a$, then $l_j'=l_j$, otherwise
	there exist $g_j$ and $r_j$ such that 
	$l_j \stackrel{g_j,a,r_j}{\longrightarrow} l_j'\in E_j$; $g=\bigwedge_{j\in S_a} g_j$
	and $r=\bigcup_{j\in S_a} r_j$.
\end{itemize}

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is that of the underlying timed automaton $\TA$
(synchronizing on synchronous and broadcast communication labels) as recalled below, 
with the following notations. 
A location is a vector $l = (l_1, \ldots, l_n)$. 
We write $l[l'_j/l_j, j\in S]$ to denote the location $l$ in which the 
$j$th element $l_j$ is replaced by $l'_j$, for all $j$ in some set $S$.
A valuation is a function $\nu$ from the set of clocks to the non-negative reals. 
Let $\mathbb{V}$ be the set of all clock valuations, and $\nu_0(x) = 0$ 
for all $x \in X$.  
We shall denote by $\nu\vDash F$ the fact that the valuation $\nu$ 
satisfies (makes true) the formula $F$.
If $r$ is a clock reset, we shall denote by $\nu[r]$ 
the valuation obtained after applying clock reset $r\subseteq X$ to $\nu$; 
and if $d\in\mathbb{R}_{> 0}$ is a delay, 
$\nu+d$ is the valuation such that, for any clock $x\in X$, 
$(\nu+d)(x)=\nu(x)+d$.

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is defined as a timed transition system $(S,s_0,\rightarrow)$,
where $S = (L_1 \times,\ldots\times L_n) \times \mathbb{V}$ is the set of states, 
$s_0 = (l^0, \nu_0)$ is the initial state, and 
$\rightarrow \subseteq S \times S$ is the transition relation defined by:
\begin{itemize}	
	%\item (silent): $(l,\nu) \rightarrow (l',\nu')$ 
	%if there exists $l_i \stackrel{g,~,r}{\longrightarrow} l'_i$, for some $i$, 
	%such that $l'=l[l'_i/l_i]$, $\nu\vDash g$ 
	%and $\nu'=\nu[r]$, 
	\item (sync): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if 
	there exist arc $l \stackrel{g,a,r}{\longrightarrow} l'\in \arcs$ 
	such that $\nu\vDash g$, $\nu'=\nu[r]$,
	for $S_a=\{j\mid 1\leq j\leq n, a\in\Sigma^s_j\}$, 
	$l'=l[l'_j/l_j, j\in S_a]$, 
	and there is no enabled transition with urgent communication label
	from $(\bar{l},\nu)$;
	
	\item (urgent): as (sync) but $a\in\Sigma^u$ and there is no delay
	if transition with urgent communication label can be taken;
	 
	\item (broadcast): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if
	there exist an output arc $l_j \stackrel{g_j,b!,r_j}{\longrightarrow} l_j'\in \arcs_j$ 
	and a (possibly empty) set of input arcs of the form
	$l_k \stackrel{g_k,b?,r_k}{\longrightarrow} l_k'\in \arcs_k$ such that 
	for all $k\in K=\{k_1,\ldots,k_m\}\subseteq\{l_1,\ldots,l_n\}\setminus\{l_j\}$,
	the size of $K$ is maximal, $\nu\vDash \bigwedge_{k\in K\cup\{j\}} g_k$,
	$l'=l[l'_k/l_k, k\in K\cup\{j\}]$ and $\nu'=\nu[r_k, k\in K\cup\{j\}]$;
	
	\item (timed): $(l,\nu)\rightarrow (l,\nu+d)$ if $\nu+d\vDash \inv(l)$. 
\end{itemize} 
%\begin{figure}[htbp]
%\centering
%\subfigure[$\TA_1\parallel \TA_2$]{
Here we exemplify timed automata usage: 
consider for instance the network of timed automata $\TA_1$ and $\TA_2$ with synchronous (non urgent) communications only:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.8, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$\stackrel{l_1}{x < 2}$}; 
\node[location]  at (4,0) (l2) {$\stackrel{l_2}{x < 2}$};
\node[left] at (-4,0) {$\TA_1$};
\node[location,double] at (0,-2) (l3) {$\stackrel{l_3}{\emptyset}$};
\node[location] at (4,-2) (l4) {$\stackrel{l_4}{\emptyset}$};
\draw[->, rounded corners] (l2) -- (5,-.5) -- (5.5,-.5) -- node[midway,right] 
				{$x>0;b;\emptyset$}  (5.5,.5) -- (5,.5)-- (l2) ;

\node[left] at (-4,-2) {$\TA_2$};
\draw[->] (l1) -- (l2) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l3) -- (l4) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l3) -- (-1,-2.5) -- (-1.5,-2.5) -- node[midway,left] 
				{$\true;a;\{x\}$}  (-1.5,-1.5) -- (-1,-1.5)-- (l3) ;
\end{tikzpicture}
\end{center}
%}
%%%
%\subfigure[$sync(\TA_1\parallel \TA_2)$]{
whose behavior is given by their synchronized product $\TA_1\parallel \TA_2$:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.9, yscale=.6,every node/.style={scale=0.7}]
\node[location]  at (0,0) (l14) {$\stackrel{(l_1,l_4)}{x < 2}$};
\node[location,double] at (3,0) (l13) {$\stackrel{(l_1,l_3)}{x < 2}$}; 
\node[location] at (6,0) (l23) {$\stackrel{(l_2,l_3)}{x < 2}$};
\node[location] at (9,0) (l24) {$\stackrel{(l_2,l_4)}{x < 2}$};
\draw[->, rounded corners] (l23) -- (5.5,1) -- (5.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (6.5,1.5) -- (6.5,1)-- (l23) ;
\draw[->] (l13) -- (l14) node[midway,above] {$x=1;c;\emptyset$};
\draw[->] (l13) -- (l23) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l23) -- (l24) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l24) -- (8.5,1) -- (8.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (9.5,1.5) -- (9.5,1)-- (l24) ;
\end{tikzpicture}
\end{center}
%}
%%%
%HK doit être modifié pour inclure des canaux broadcast
%\subfigure[A possible run]{
and where a possible run is:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node at (0,0) (e1) {$[(l_1,l_3);x=0]$}; // t+1
\node at (2,0) (e2) {$[(l_1,l_3);x=1]$}; // a
\node at (4,0) (e3) {$[(l_2,l_3);x=0]$}; // t+.5
\node at (6,0) (e4) {$[(l_2,l_3);x=.5]$}; // b
\node at (8,0) (e5) {$[(l_2,l_3);x=.5]$}; // t+.5
\node at (10,0) (e6) {$[(l_2,l_4);x=1]$}; 
\draw[->] (e1) -- (e2) ;
\draw[->] (e2) -- (e3) ;
\draw[->] (e3) -- (e4) ;
\draw[->] (e4) -- (e5) ;
\draw[->] (e5) -- (e6) ;
\end{tikzpicture}
\end{center}
%}
%\caption{A network of timed automata with a possible run.}
%\label{fig:ta}
%\end{figure}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{\bf Encoding into timed automata.}
We are now ready to introduce the encoding of the high-level Petri net formalization of $\andy$, to this aim we need to add some notation:

 \begin{newnotation}
Let $\Tag=\{\beta_1,\ldots,\beta_n\}$ be the set of all \obligatory activities identifiers from $\Syn$,
ordered alphabetically, \ie $\beta_i<\beta_j$ if $i<j$. 
We denote by 
\[
\Tag^{\circledast}=\{ seq(h) \mid h\in \mathcal{P}(\Tag) \wedge h\neq\emptyset \} \cup \{ \varepsilon\},
\] 
the set of sequences $seq(h)$ obtained by concatenating the identifiers in non-empty subsets $h$ of $\Tag$, where for each $h=\{\beta_{i_1},\ldots,\beta_{i_m}\mid \forall j,k:~ i_j<i_k \}\in \mathcal{P}(\Tag)$, $seq(h)=\beta_{i_1}\cdots \beta_{i_m}$. We assume that if $\Tag^{\circledast}=\{h_1 \mydots h_k\}$, then the $h_i$'s are ordered by decreasing length and alphabetically in such a way that $h_1=\beta_1\cdots\beta_{|\Tag|}$ and $h_k = \varepsilon$. 

Moreover, $\beta_i=h[i]$ is the identifier at the $i$-position, and  $h=h_1-h_2$ is  the sequence of identifier in $h_1$ without those in $h_2$.
  %Let $Lab$ be a set of labels, we denote with 
  %$$Lab^{\circledast} = \{x_1 \cdots x_n \mid n \in [1..|Lab|], \forall i,j \in [1..n], x_i \in Lab \wedge x_i < x_j  \} \cup \{ \varepsilon\}$$ 
  %the set of labels obtained by concatenating in alphabetical order ($<$) the labels in $Lab$, using them at most once.  
  %
  %Labels in $Lab^{\circledast} $ can be alphabetically ordered from the longest to $\varepsilon$ thus we denote  $Lab^{\circledast} = \{t_1 \mydots t_n \} $ where $t_1$ is the word composed of all labels in $Lab$ and $t_n = \varepsilon$. 
 \end{newnotation}

 The encoding of an $\andy$ network is the synchronized product of one timed automaton for each entity in \entities  together with a set of auxiliary automata that are used to handle \potential and \obligatory activities.  
 The idea is that the global state of an \andy network is divided into its local counterparts represented by state of entities (\ie their levels). Thus for each entity $\entity$ we build a timed automaton $\TA(\entity, \level{\entity})$ which has as many locations as the levels in $\entity$. Auxiliary automata are used to implement the encoding of places $p_{\rho}$ ($\TA(\rho)$ for $\rho \in \Syn \cup \Reac$) and to realize time progression together with \obligatory activities ($\TA_{\tick}$). 
 More formally:
 
 \begin{definition} Given an \andy network $(\entities, \Syn, \Reac)$, with initial expression level $\level{\entity}$ for each $\entity \in \entities$, the corresponding timed automata encoding is 
 \[\enc{(\entities, \Syn, \Reac)} = \prod_{\entity \in \entities} \TA(\entity,\level{\entity}) \parallel \prod_{\alpha \in  \Reac} \TA(\alpha) \parallel \prod_{\beta \in \Syn} \TA(\beta) \parallel \TA_{\tick} \]  
 where $\TA(\entity, \level{\entity})$, $\TA(\alpha)$,$\TA(\beta)$  and $\TA_{\tick}$ are defined next. In the following we assume $ \Tag $ to be the set of identifiers of \obligatory activities in $\Syn$. 
 \paragraph{\bf Entities.}
 $\TA(\entity, \level{\entity}) = (L_{\entity},l^0_{\entity},X_{\entity},\Sigma_{\entity}, \arcs_{\entity} ,\inv_{\entity})$
  where:
  \begin{itemize}
   \item $L_{\entity}=\{l^{\entity}_i \mid i \in [0 \mydots \setlev_{\entity} ]\} \cup \{k_i^h,k_i^{d,h} \mid i \in [0 \mydots \setlev_{\entity} ], h\in \Tag^{\circledast} \}$ with  $l^0_{\entity} = l^{\entity}_{\level{\entity}}$
   \item $X_{\entity}=\{\birth^{\entity}_i, \refr^{\entity}_i \mid i \in [0 \mydots \setlev_{\entity} ]\} \cup \{x_{\entity}\}$
   \item $\Sigma^s_{\entity} =  \{  \alpha \mid \alpha \text{ identifier of an activity in }  \Reac  \}$, $  \Sigma_{\entity}^b =  \Tag^{\circledast}$, $\Sigma_{\entity}^u =  \{\tick h \mid h \in \Tag^{\circledast} \} $ 
   \item $\arcs_{\entity} = \arcs_{\Reac} \cup \arcs_{\Syn}$ where 
$$
\arcs_{\Reac}\! =\! \{ l_j \xrightarrow{g(A_{\alpha}) \wedge g(I_{\alpha}) \wedge x_{\entity} = 0, \alpha, r} l_e \mid \entity_{A_{\alpha}} \leq j < \entity_{I_{\alpha}}, \alpha \in \Reac, \entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}  
$$
with  $j, e, \entity_{A_{\alpha}}$, and $\entity_{I_{\alpha}}$ are levels of $\entity$ defined as follows:
    
    $$\entity_{A_{\alpha}} = \begin{cases}
                \level{a} & \text{if } (\entity, \level{a}) \in {A_{\alpha}}     \\
                0 & \text{otherwise}
               \end{cases}
\qquad 
\entity_{I_{\alpha}} = \begin{cases}
               \level{i} & \text{if } (\entity, \level{i}) \in {I_{\alpha}}\\
                \setlev_{\entity} & \text{otherwise}
               \end{cases}
$$

$$ g(A_{\alpha}) = \begin{cases}
\birth^{\entity}_{\level{a}} \geq \dur{\alpha} & \text{if } (\entity, \level{a}) \in A_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
\ 
g(I_{\alpha}) = \begin{cases}
\birth^{\entity}_{\level{i}} \geq \dur{\alpha} & \text{if } (\entity, \level{i}) \in I_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
$$

$$m = \begin{cases}
               \max(0, \min(j+v, \setlev_{\entity}-1)) & \text{if } (\entity, v) \in R_{\alpha} \\
                j & \text{otherwise}
               \end{cases}
$$

$$r = \begin{cases}
        \emptyset & \text{if } (\entity, v) \not \in R_{\alpha}  \\
        \{u^\entity_m,\} \cup \{\birth_x^{\entity} \mid x \in [j+1,m]\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge m-j>0\\
        \{u^\entity_m,\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge m-j=0\\
        \{u^\entity_m,\} \cup \{\birth_x^{\entity} \mid x \in [m+1,j]\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge m-j<0
      \end{cases}
$$
$$
\begin{array}{ll}
 \arcs_{\Syn} = & \{ l_j \xrightarrow{g(d)\wedge g , h?, \emptyset} k_j^{d,h},  \mid  j \in [0\mydots\setlev_{\entity}-1], h\in \Tag^{\circledast}\} \ \cup \\
               & \{ l_j \xrightarrow{\neg g(d)\wedge g , h?, \emptyset} k_j^h,  \mid  j \in [0\mydots\setlev_{\entity}-1], h\in \Tag^{\circledast}\} \ \cup \\
              & \{ k_j^{d,h} \xrightarrow{\true, h', r \cup \{x_{\entity}\} } l_e,  \mid  j \in [0\mydots\setlev_{\entity}-1], h,h' \in \Tag^{\circledast}, h<h' \}\ \cup \\ 
              & \{ k_j^h \xrightarrow{\true, \tick h', r'\cup \{x_{\entity}\} } l_e',  \mid  j \in [0\mydots\setlev_{\entity}-1], h,h' \in \Tag^{\circledast}, h<h' \}
\end{array}
$$
where
$$\begin{array}{lcl}
   g & = & \! \bigwedge_{k=1}^{n} g(\beta_k)  \wedge \bigwedge_{k=1}^{m} \neg g(\beta'_m)\text{ for } h=\beta_1 \cdots \beta_n \text{ and } h_1- h= \beta'_1 \cdots \beta'_m \\
   g(\beta) & = & g'(A_\beta) \wedge g'(I_\beta) \text{ and } \beta= \activ{A_\beta}{I_\beta}{\dur{\beta}}{R_\beta}\\
   g(d) & = & u_j > \life_{\entity}(j)
  \end{array}
$$    


$$ g'(A_\beta) = \begin{cases}
j \geq \level{a} \wedge \birth^{\entity}_{\level{a}} \geq \dur{\beta} & \text{if } (\entity, \level{a}) \in A_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
g'(I_\beta) = \begin{cases}
j<\level{i} \wedge \birth^{\entity}_{\level{i}} \geq \dur{\beta} & \text{if } (\entity, \level{i}) \in I_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
\begin{array}{lcl}
m & = & \max(0, \min(\sum_{i\in[1 \mydots n]} f(h[i]') +j -1, \setlev_{\entity}-1)) \\
m' & = & \max(0, \min(\sum_{i\in[1\mydots n]} f(h[i]')+j, \setlev_{\entity}-1)) \\
 & & \mbox{ where } f(h[i]) = \begin{cases}
        v & \text{if }  (\entity, v) \in R_{\beta_i} \\
        0 & \text{otherwise} 
       \end{cases}
\end{array}
$$
\[
\begin{array}{ll}
r = &\begin{cases}
        \{u^\entity_m\} \cup \{\birth_x^{\entity} \mid x \in [j+1,m]\} & \text{if }  m-j>0\\
        \{u^\entity_m\} & \text{if }   m-j=0 \\
        \{u^\entity_m\} \cup \{\birth_x^{\entity} \mid x \in [m+1,j]\} & \text{if }   m-j<0     
      \end{cases}
      \\
r' = &\begin{cases}
        \{u^\entity_{m'}\} \cup \{\birth_x^{\entity} \mid x \in [j+1,m']\} & \text{if }  m'-j>0\\
        \{u^\entity_{m'}\} & \text{if }  \entity \in h'  \wedge m'-j=0 \\
        \{u^\entity_{m'}\} \cup \{\birth_x^{\entity} \mid x \in [m'+1,j]\} & \text{if }   m'-j<0 \\
        \emptyset & \text{if }  \entity \notin h' 
      \end{cases}
\end{array}
     \]
where $\entity \in h$ denotes formula: $\exists \beta_k=\activ{A_{\beta_k}}{I_{\beta_k}}{\dur{\beta_k}}{R_{\beta_k}}$ s.t. $h=\beta_1\cdots \beta_n, 1\leq k \leq n \wedge (\entity, v) \in R_{\beta_k}$ 
    
   \item $Inv_{\entity}(l^{\entity}_i) = \refr^{\entity}_i \leq \life_{\entity}(i)$ for all $i \in [0 \mydots \setlev_{\entity}]$
   
  \end{itemize}

  \paragraph{\bf \Potential activity.}
$\TA(\alpha) = (L_{\alpha},l^0_{\alpha},X_{\alpha},\Sigma_{\alpha},\arcs_{\alpha},\inv_{\alpha})$  for $\alpha \in \Reac$ where
  \begin{itemize}
  \item $L_{\alpha}=\{l_\alpha\}$,  $l^0_{\alpha} = \alpha$, $X_{\alpha}= \{w_{\alpha}\}$,  $\Sigma^s_{\alpha} = \{ \alpha \} $
  \item $\arcs_{\alpha} = \{ l_\alpha \xrightarrow{w_{\alpha} \geq  \dur{\alpha}, \alpha, \{ w_{\alpha}\}} l_\alpha \}$
  \item $\inv_{\alpha}(l_{\alpha}) = \true$.
  \end{itemize}
  
  \paragraph{\bf \Obligatory activity.} $\TA(\beta) = (L_{\beta},l^0_{\beta},X_{\beta},\Sigma_{\beta},\arcs_{\beta},\inv_{\beta})$  for $\beta \in \Syn$ where
  \begin{itemize}
   \item $L_{\beta}=\{l_\beta, l'_\beta\}$,  $l^0_{\beta} = l_\beta$,  $X_{\beta}= \{w_{\beta}\}$,  $\Sigma_{\beta}^b =  \Tag^{\circledast}$,  $
\Sigma_{\beta}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\beta} = \{ l_\beta \xrightarrow{w_{\beta} \geq  \dur{\beta}, h?, \emptyset} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \} \cup \{ l'_\beta \xrightarrow{\true, \tick h, \{w_{\beta}\}} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \}$
   \item $\inv_{\beta}(l_{\beta}) = \true$ and $\inv_{\beta}(l'_{\beta}) = \true$.
  
  \end{itemize}
  
  \paragraph{\bf Time.}  $\TA_{\tick} = (L_{\tick},l^0_{\tick},X_{\tick},\Sigma_{\tick},\arcs_{\tick},\inv_{\tick})$ where
  \begin{itemize}
   \item $L_{\tick}=\{l_h \mid h \in \Tag^{\circledast}\} \cup \{l_{\bot}\}$,  $l^0_{\tick} = l_{h_1}$,  $X_{\tick}= \{x\}$, $\Sigma_{\tick}^b =  \Tag^{\circledast}$, $ 
\Sigma_{\tick}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\tick} =\begin{array}{l}
 \{l_{h_i} \xrightarrow{x=1, h_i!, \emptyset } l_{h_i+1}, l_{h_i+1} \xrightarrow{\true, \tick h_i, \{x\} } l_{h_1} \mid h,  i \in [1\mydots n-1]   \}  \\
\cup \ \{ l_{h_n} \xrightarrow{x=1, h_n!, \emptyset } l_{\bot}, l_{\bot} \xrightarrow{\true, \tick\varepsilon, \{x\} } l_{h_1}   \}
                  \end{array}
$
   \item $\inv_{\tick}(l) = \true$ for all $l \in L_{\tick}$.
  
  \end{itemize}
  
  
  
 \end{definition}

 
  \begin{theorem}
The encoding of  \andy network $(\entities, \Syn, \Reac)$
%its encoding $\enc{(\entities, \Syn, \Reac)}$, 
is correct and complete.\looseness=-1
\end{theorem}
\begin{proof}[Sketch]
 Follows by induction on the length of the run and from a case analysis on the transition performed. 
 
Some intuitions on the proof follows. For each entity $\entity$, the corresponding marking of place $p_{\entity}$, $M(p_{\entity})=\tuple{\lev_{\entity}, \refr_{\entity}, \birth_{\entity}}$, in the Petri net representation is encoded by    
 the state (location $l^{\entity}_{\lev_{\entity}}$ and valuations of clocks variables $\refr^{\entity}_{\lev_{\entity}}, \birth^{\entity}_i$ for $i \in [0\mydots\setlev_{\entity} -1]$) of each timed automaton $\TA(\entity, \level{\entity})$. Marking of places $p_{\rho}$ (for $\rho \in \Syn \cup \Reac$) is given by the valuation of clock $w_{\rho}$ in the corresponding timed automaton $\TA(\rho)$.
 
 Each transition of the Petri net is encoded by (a series of) timed automata arcs.
 For each transition $t_{\alpha}$ (corresponding to  \potential activity  $\alpha$) involving $\entity$ there is a (synchronous) arcs in the timed automaton $\TA(\entity, \level{\entity})$ whose guard describes its role in the activity (activator, inhibitor or result). Clock $w_{\alpha}$ in   $\TA(\alpha)$ implements the constraint that the activity $\alpha$ is performed at most once in the interval $\dur{\alpha} $:  $w_{\alpha} \geq \dur{\alpha}$. 
 This way, the synchronous product of all automata reconstructs the full guard of the activity $\alpha$ and  exactly one  transition in the synchronized product of automata corresponds to the firing of transition $t_{\alpha}$. The state reached after this transition coincides with the corresponding marking in the Petri net.
 
 Transition $t_c$ is trickier as time progression causes  decay but more importantly the simultaneous action of \obligatory activities.
 Notice that \obligatory activities concern the global state of an \andy network (the maximal set of enabled \obligatory activities has to be performed each time $t_c$ fires) but each sub-automaton of the synchronized automaton as only a partial/local information.  
 That is why, we need to introduce the auxiliary automaton $\TA_{\tick}$ that coordinates and gathers partial information from all  other automata.
 Thus, the implementation of $t_c$ has two phases. The first one gathers partial information, performs the selection of the largest set of enabled \obligatory activities and forces the time to progress in a discrete fashion;  the second phase completes the time progression and synchronizes all timed automata communicating the chosen maximal set of \obligatory activities.
 Both phases are initiated by   automaton $\TA_{\tick}$ which has two types of arcs: broadcast ones for the first phase and urgent synchronous ones for the second (see Figure \ref{fig:tick}).
\begin{figure}[t]
\centering
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$l_{\beta_1\beta_2}$}; 
\node[location]  at (2,0) (l2) {$l_{\beta_1}$};
\node[location]  at (4,0) (l3) {$l_{\beta_2}$};
\node[location]  at (6,0) (l4) {$l_{\epsilon}$};
\node[location]  at (8,0) (l5) {$l_{\bot}$};
\draw[->] (l1) -- node[midway,above] {$\beta_1\beta_2!$} (l2) ;
\draw[->] (l2) -- node[midway,above] {$\beta_1!$} (l3) ;
\draw[->] (l3) -- node[midway,above] {$\beta_2!$} (l4) ;
\draw[->] (l4) -- node[midway,above] {$\epsilon!$} (l5) ;
\draw[->, rounded corners] (l2) -- node[midway,right] {$\tick\beta_1\beta_2$}(2,1.5) -- (1,1.5) --  (l1) ;
\draw[->, rounded corners] (l3) -- node[midway,right] {$\tick\beta_1$}(4,2) -- (1,2) --  (l1) ;
\draw[->, rounded corners] (l4) -- node[midway,right] {$\tick\beta_2$}(6,2.5) -- (1,2.5) --  (l1) ;
\draw[->, rounded corners] (l5) -- node[midway,right] {$\tick\epsilon$}(8,3) -- (1,3) --  (l1) ;

\end{tikzpicture}
\caption{The shape of timed automaton $\TA_\tick$ for $\Tag^\circledast=\{\beta_1\beta_2,\beta_1,\beta_2,\epsilon\}$, where $\tick\beta_1\beta_2$, $\tick\beta_1$, $\tick\beta_2$, $\tick\epsilon$ are all synchronous urgent communication labels.}
\label{fig:tick}
\end{figure}
More precisely, $\TA_{\tick}$ progressively interrogates the entities timed automata $\TA(\entity, \level{\entity})$ and the \obligatory activities automata $\TA(\beta_i)$ to ``compute'' for each automaton the maximal set of enabled \obligatory activities. This is obtained through broadcast arcs labeled with sequences of \obligatory activities identifiers $h\in\Tag^\circledast$, from the longest ($h=seq(\Tag)=\beta_1\cdots\beta_n$) to the shortest ($h=\epsilon$, \ie no \obligatory activity is enabled).
 As broadcast is a non blocking transition and because of the ordering on sequences in $\Tag^\circledast$, each entity automaton chooses its maximal set of \obligatory activities it is involved in. If it is necessary, it also performs decay. When all automata $\TA(\entity, \level{\entity})$ and $\TA(\beta_{i})$ have agreed on some sequence $h=\beta_{i_1} \mydots \beta_{i_m}$ (in the worst case $h$ is empty) the first phase is completed and $\{ \beta_{i_1},  \mydots,  \beta_{i_m}\}$ is the largest set of enabled \obligatory activities. The second phase is then implemented with an urgent synchronous arc synchronizing all automata: $\TA_{\tick}$, $\TA(\entity, \level{\entity})$, for each $\entity \in \entities$, and $\TA(\beta_i)$, for $i\in [i_1 \mydots i_m]$.
 Notice that guards on broadcast transitions constraint the clocks to progress by one time unit at once.   
 As a consequence, at the end of the two phase algorithm, timed automata of entities and of places $p_{\rho}$ together with the  corresponding clocks valuations exactly encode the marking reached after firing $t_c$. 
 \qed
\end{proof}


